0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 14 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 20 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
flB_in_gag([], [], 0) → flB_out_gag([], [], 0)
flB_in_gag(.(T8, T9), T12, s(T11)) → U3_gag(T8, T9, T12, T11, pA_in_gaagg(T8, X13, T12, T9, T11))
pA_in_gaagg([], T18, T18, T9, T11) → U1_gaagg(T18, T9, T11, flB_in_gag(T9, T18, T11))
U1_gaagg(T18, T9, T11, flB_out_gag(T9, T18, T11)) → pA_out_gaagg([], T18, T18, T9, T11)
pA_in_gaagg(.(T25, T26), X38, .(T25, T28), T9, T11) → U2_gaagg(T25, T26, X38, T28, T9, T11, pA_in_gaagg(T26, X38, T28, T9, T11))
U2_gaagg(T25, T26, X38, T28, T9, T11, pA_out_gaagg(T26, X38, T28, T9, T11)) → pA_out_gaagg(.(T25, T26), X38, .(T25, T28), T9, T11)
U3_gag(T8, T9, T12, T11, pA_out_gaagg(T8, X13, T12, T9, T11)) → flB_out_gag(.(T8, T9), T12, s(T11))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
flB_in_gag([], [], 0) → flB_out_gag([], [], 0)
flB_in_gag(.(T8, T9), T12, s(T11)) → U3_gag(T8, T9, T12, T11, pA_in_gaagg(T8, X13, T12, T9, T11))
pA_in_gaagg([], T18, T18, T9, T11) → U1_gaagg(T18, T9, T11, flB_in_gag(T9, T18, T11))
U1_gaagg(T18, T9, T11, flB_out_gag(T9, T18, T11)) → pA_out_gaagg([], T18, T18, T9, T11)
pA_in_gaagg(.(T25, T26), X38, .(T25, T28), T9, T11) → U2_gaagg(T25, T26, X38, T28, T9, T11, pA_in_gaagg(T26, X38, T28, T9, T11))
U2_gaagg(T25, T26, X38, T28, T9, T11, pA_out_gaagg(T26, X38, T28, T9, T11)) → pA_out_gaagg(.(T25, T26), X38, .(T25, T28), T9, T11)
U3_gag(T8, T9, T12, T11, pA_out_gaagg(T8, X13, T12, T9, T11)) → flB_out_gag(.(T8, T9), T12, s(T11))
FLB_IN_GAG(.(T8, T9), T12, s(T11)) → U3_GAG(T8, T9, T12, T11, pA_in_gaagg(T8, X13, T12, T9, T11))
FLB_IN_GAG(.(T8, T9), T12, s(T11)) → PA_IN_GAAGG(T8, X13, T12, T9, T11)
PA_IN_GAAGG([], T18, T18, T9, T11) → U1_GAAGG(T18, T9, T11, flB_in_gag(T9, T18, T11))
PA_IN_GAAGG([], T18, T18, T9, T11) → FLB_IN_GAG(T9, T18, T11)
PA_IN_GAAGG(.(T25, T26), X38, .(T25, T28), T9, T11) → U2_GAAGG(T25, T26, X38, T28, T9, T11, pA_in_gaagg(T26, X38, T28, T9, T11))
PA_IN_GAAGG(.(T25, T26), X38, .(T25, T28), T9, T11) → PA_IN_GAAGG(T26, X38, T28, T9, T11)
flB_in_gag([], [], 0) → flB_out_gag([], [], 0)
flB_in_gag(.(T8, T9), T12, s(T11)) → U3_gag(T8, T9, T12, T11, pA_in_gaagg(T8, X13, T12, T9, T11))
pA_in_gaagg([], T18, T18, T9, T11) → U1_gaagg(T18, T9, T11, flB_in_gag(T9, T18, T11))
U1_gaagg(T18, T9, T11, flB_out_gag(T9, T18, T11)) → pA_out_gaagg([], T18, T18, T9, T11)
pA_in_gaagg(.(T25, T26), X38, .(T25, T28), T9, T11) → U2_gaagg(T25, T26, X38, T28, T9, T11, pA_in_gaagg(T26, X38, T28, T9, T11))
U2_gaagg(T25, T26, X38, T28, T9, T11, pA_out_gaagg(T26, X38, T28, T9, T11)) → pA_out_gaagg(.(T25, T26), X38, .(T25, T28), T9, T11)
U3_gag(T8, T9, T12, T11, pA_out_gaagg(T8, X13, T12, T9, T11)) → flB_out_gag(.(T8, T9), T12, s(T11))
FLB_IN_GAG(.(T8, T9), T12, s(T11)) → U3_GAG(T8, T9, T12, T11, pA_in_gaagg(T8, X13, T12, T9, T11))
FLB_IN_GAG(.(T8, T9), T12, s(T11)) → PA_IN_GAAGG(T8, X13, T12, T9, T11)
PA_IN_GAAGG([], T18, T18, T9, T11) → U1_GAAGG(T18, T9, T11, flB_in_gag(T9, T18, T11))
PA_IN_GAAGG([], T18, T18, T9, T11) → FLB_IN_GAG(T9, T18, T11)
PA_IN_GAAGG(.(T25, T26), X38, .(T25, T28), T9, T11) → U2_GAAGG(T25, T26, X38, T28, T9, T11, pA_in_gaagg(T26, X38, T28, T9, T11))
PA_IN_GAAGG(.(T25, T26), X38, .(T25, T28), T9, T11) → PA_IN_GAAGG(T26, X38, T28, T9, T11)
flB_in_gag([], [], 0) → flB_out_gag([], [], 0)
flB_in_gag(.(T8, T9), T12, s(T11)) → U3_gag(T8, T9, T12, T11, pA_in_gaagg(T8, X13, T12, T9, T11))
pA_in_gaagg([], T18, T18, T9, T11) → U1_gaagg(T18, T9, T11, flB_in_gag(T9, T18, T11))
U1_gaagg(T18, T9, T11, flB_out_gag(T9, T18, T11)) → pA_out_gaagg([], T18, T18, T9, T11)
pA_in_gaagg(.(T25, T26), X38, .(T25, T28), T9, T11) → U2_gaagg(T25, T26, X38, T28, T9, T11, pA_in_gaagg(T26, X38, T28, T9, T11))
U2_gaagg(T25, T26, X38, T28, T9, T11, pA_out_gaagg(T26, X38, T28, T9, T11)) → pA_out_gaagg(.(T25, T26), X38, .(T25, T28), T9, T11)
U3_gag(T8, T9, T12, T11, pA_out_gaagg(T8, X13, T12, T9, T11)) → flB_out_gag(.(T8, T9), T12, s(T11))
FLB_IN_GAG(.(T8, T9), T12, s(T11)) → PA_IN_GAAGG(T8, X13, T12, T9, T11)
PA_IN_GAAGG([], T18, T18, T9, T11) → FLB_IN_GAG(T9, T18, T11)
PA_IN_GAAGG(.(T25, T26), X38, .(T25, T28), T9, T11) → PA_IN_GAAGG(T26, X38, T28, T9, T11)
flB_in_gag([], [], 0) → flB_out_gag([], [], 0)
flB_in_gag(.(T8, T9), T12, s(T11)) → U3_gag(T8, T9, T12, T11, pA_in_gaagg(T8, X13, T12, T9, T11))
pA_in_gaagg([], T18, T18, T9, T11) → U1_gaagg(T18, T9, T11, flB_in_gag(T9, T18, T11))
U1_gaagg(T18, T9, T11, flB_out_gag(T9, T18, T11)) → pA_out_gaagg([], T18, T18, T9, T11)
pA_in_gaagg(.(T25, T26), X38, .(T25, T28), T9, T11) → U2_gaagg(T25, T26, X38, T28, T9, T11, pA_in_gaagg(T26, X38, T28, T9, T11))
U2_gaagg(T25, T26, X38, T28, T9, T11, pA_out_gaagg(T26, X38, T28, T9, T11)) → pA_out_gaagg(.(T25, T26), X38, .(T25, T28), T9, T11)
U3_gag(T8, T9, T12, T11, pA_out_gaagg(T8, X13, T12, T9, T11)) → flB_out_gag(.(T8, T9), T12, s(T11))
FLB_IN_GAG(.(T8, T9), T12, s(T11)) → PA_IN_GAAGG(T8, X13, T12, T9, T11)
PA_IN_GAAGG([], T18, T18, T9, T11) → FLB_IN_GAG(T9, T18, T11)
PA_IN_GAAGG(.(T25, T26), X38, .(T25, T28), T9, T11) → PA_IN_GAAGG(T26, X38, T28, T9, T11)
FLB_IN_GAG(.(T8, T9), s(T11)) → PA_IN_GAAGG(T8, T9, T11)
PA_IN_GAAGG([], T9, T11) → FLB_IN_GAG(T9, T11)
PA_IN_GAAGG(.(T25, T26), T9, T11) → PA_IN_GAAGG(T26, T9, T11)
From the DPs we obtained the following set of size-change graphs: